D:Dsys, i:Id, s1, s2:M(i).(timed)state, k1, k2:Knd, v1:d-decl(D;i)(k1), v2:d-decl(D;i)(k2),
m1:({m:M(i).Msg| source(mlnk(m)) = i}  List).
Feasible(D)
 (<s1, doact(k1;v1), m1> = next-world-state(D;i;s2;k2;v2)  d-world-state(D;i))
 {s1 = shift-state(x.M(i).ef(k2,x,read-state(s2),v2)?s2(x))
 & k1 = k2
 & v1 = v2  d-decl(D;i)(k2)
 & m1 = filter(m.source(mlnk(m)) = i;M(i).sends(k2,read-state(s2),v2))} 

latex

Definitions	M(i), M.Msg, M.sends(k,s,v), filter(P;l), <a, b>, Id, s = t, {x:A| B(x)} , type List, d-decl(D;i), f(a), Knd, P & Q, mlnk(m), x:A. B(x), source(l), Action(dec), x:A  B(x), x.A(x), x. t(x), t.1, t.2, M.(timed)state, next-world-state(D;i;s;k;v), d-world-state(D;i), doact(k;v), x:AB(x), S  T, P  Q, , Feasible(D), Dsys, {T}, Void, Type, t  T, Unit
Lemmas	inr equal, unit wf, dsys wf, Knd wf, d-feasible wf, d-world-state wf, next-world-state wf, doact wf, ma-tst wf, pi2 wf, pi1 wf, action wf, d-decl wf, ma-msg wf, d-m wf, Id wf, lsrc wf, mlnk wf d